1. Field of the Invention
The present invention relates in general to tools for verifying integrated circuit designs and in particular to a tool employing a simulator for verifying properties of a circuit design.
2. Description of Related Art
An integrated circuit (IC) design engineer normally models an IC using a hardware description language (HDL) to describe the behavior of the various components making up a circuit and the manner in which those components interact. The design engineer typically uses a circuit simulator to simulate circuit behavior based on the HDL model to verify that the circuit will behave as expected before the IC is fabricated based on the HDL model.
A circuit simulator simulates the behavior of a circuit based on the HDL description of the circuit as it would respond over time to a sequence of input signals. The simulator can produce output waveform data representing the behavior of the circuit's output signals as well as the circuit's “internal” signals that would not appear at the circuit's output terminals. In addition to providing a simulator with the HDL description of the circuit to be simulated, the design engineer also provides the simulator with a “test bench”, a data file describing the time-varying behavior of input signals that are to stimulate the circuit. The test bench also indicates the various circuit output and internal signals that are to be monitored during the simulation to determine whether the simulated circuit is behaving as expected. Thus a simulation verifies whether a circuit described by an HDL file will respond as expected to a particular sequence of input signal states specified by the test bench.
Design engineers often like to verify that a circuit has one or more particular properties. We say a circuit possesses a “property” if it always exhibits a particular consequent behavior following a particular antecedent event. An “antecedent event” can be any particular pattern in any combination of the circuit's input, output and internal signals. A “consequent event” can be any particular pattern in any combination of the circuit's output and internal signals. Note that a consequent behavior involves only the signals that the circuit generates (output and internal) and does not involve the input signals that the circuit receives. Thus once an antecedent event occurs, the circuit having a particular property will exhibit the consequent behavior regardless of the behavior of its input signals following the antecedent event. To fully verify that a circuit has a particular property, we must verify that the circuit will exhibit a particular consequent behavior in response to an antecedent event regardless of the behavior of any of its input signals following the antecedent event.
When the antecedent event is defined only in terms of the circuit's input signals, the circuit must exhibit the consequent behavior regardless of its current state when the antecedent event occurs. For example suppose a circuit has the property of responding to an input RESET signal (an antecedent event) by generating an ACKNOWLEDGE signal two clock cycles after receiving the RESET signal (a consequent behavior). Thus regardless of the state of the circuit when it receives the RESET signal, it will generate the ACKNOWLEDGE signal two clock cycles later.
To use a simulator to completely verify that a circuit has such a property, a design engineer would have to prepare a test bench capable of driving the circuit to every possible state and applying the RESET signal to determine whether the circuit would produce an ACKNOWLEDGE signal two cycles later. Since the circuit would have input signals other than the RESET signal, the test bench would also have to test every possible combination of input signal behavior after the RESET signal is asserted to determine whether any such combination would prevent the circuit from generating the ACKNOWLEDGE signal two cycles after the RESET signal. Preparing such a test bench is normally not feasible for even modestly complex circuits because complex circuits can exist in a very large number of possible (“reachable”) states and can have a large number of input signals. A design engineer might also have much difficulty determining how to drive a circuit to every reachable state. In any case such a simulation would likely take too much processing time. Thus a circuit simulator is usually not a good tool for completely verifying that a complex circuit has a particular property.
A conventional “state space generation” tool generates a “state space” model of a circuit design such as a binary decision diagram (BDD) representing all of the states the circuit can reach from its initial state and indicating the input signal events that cause the circuit to transition between states. A conventional “state space model analysis” tool can analyze a state space model to locate each occurrence of a particular antecedent event and to determine whether in all cases the circuit will exhibit a particular consequent behavior in response to each antecedent event. Thus state space generation and analysis tools can completely verify a circuit property. Since such tools work automatically, they free the design engineer from having to develop a complicated test bench to verify a circuit property. However even a moderately complex circuit can have such an enormous number of reachable states that a state space generation and analysis tool usually requires an impractically large amount of processing time and resources to verify a circuit property.
Thus as a practical matter, a circuit simulator can normally only partially verify a property of a complex circuit. And while state space model generation and analysis tools can completely verify a circuit property, they can do so only for relatively simple circuits.
What is needed is a practical system for verifying a property of a complex circuit with a greater degree of certainty than is feasible using a simulator, but with greater speed than is possible using conventional state space model generation and analysis tools.